ds1, ds2:x:Id fp Type. Normal(ds1)  Normal(ds2)  Normal(ds1  ds2) 

latex

Definitions	False, P  Q, A, left+right, P  Q, b, x:A. B(x), t  T, b, , s = t, Prop, Id, Type, x.A(x), x. t(x), Top, a:A fp B(a), x:AB(x), IdDeq, x  dom(f), x:AB(x), P & Q, P  Q, Unit, Void, x:A. B(x), f  g, f(x), Normal(T), xdom(f). v=f(x)   P(x;v), Normal(ds)
Lemmas	normal-ds wf, fpf wf, fpf-join wf, top wf, fpf-join-ap-sq, fpf-join-dom, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, Id wf, bool wf, bnot wf, not wf, assert wf